$\forall$$L$:Id List, ${\it ds}$, ${\it init}$:Top, $i$:Id.
\\[0ex]([[$\oplus$$x$$\in$$L$.@$i$ $x$ initially ${\it init}$($x$):${\it ds}$($x$)]]($i$))
\\[0ex]$\sim$
\\[0ex]mk{-}ma(reduce($\lambda$$x$,$f$. $x$ : ${\it ds}$($x$) $\oplus$ $f$;;$L$);
\\[0ex];
\\[0ex]reduce($\lambda$$x$,$f$. $x$ : ${\it init}$($x$) $\oplus$ $f$;;$L$);
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex])